\begin{tabbing}
$\forall$$T$:Type, ${\it as}$:$T$ List, $f$, $g$:($T$$\rightarrow\mathbb{B}$).
\\[0ex]$T$ $\subseteq\rho$ $\mathbb{Z}$
\\[0ex]$\Rightarrow$ sorted(${\it as}$)
\\[0ex]$\Rightarrow$ (\=priority{-}select($f$;$g$;${\it as}$) $=$ inl(false$_{2}$) $\in$ $\mathbb{B}$+Unit\+
\\[0ex]$\Leftrightarrow$
\\[0ex]($\exists$$a$$\in$${\it as}$.$g$($a$) \& ($\forall$$b$:$T$. ($b$ $\in$ ${\it as}$) $\Rightarrow$ $b$$\leq$$a$ $\Rightarrow$ $\neg$$f$($b$))))
\-
\end{tabbing}